COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	.BEGIN DOUBLE SPACE
 00004 ENDMK
⊗;
.BEGIN DOUBLE SPACE
1-III. GETTING ALONG WITH THE SYSTEM.

1) Running the prover.

RU PROVER [P,JRA]

(PROVE | TRY  <input>)   <input> is either DSK: <file> or null.

2) Saving a core image.

.BEGIN VERBATIM
	Hit space bar and wait for response(*).

	The prover responds by typing its first clause.

	Now type HALT.

	Response: "HALT AT USER ####".

	You may now save the core image.

	Typing "ST" or "RUN"-ing the saved image will
	have the same effect: the prover will respond
	"*" and you will be back in the on-line editor.
	You may continue the proof search by typing
	"CONTINUE".
.END

3) Reallocation.

Frequently it is desirable to increase the storage areas during the
execution of the prover without having to restart the whole problem.
This can be done as follows:

.BEGIN VERBATIM
	Hit the space bar and wait for response.

	Call the monitor.

	Execute "ST 141".

	Call the monitor.

	Execute "CORE #".

	Execute "ST".

	Evaluate "(REENTER)".

	The prover will now resume its computation
	in the enlarged work spaces.
.END
.END